COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	reiter[f82,jmc]		To Reiter re circumscription applied to Nixon paradox
C00009 00003	Perhaps we want to say things like
C00011 00004	Some thoughts on circumscription:
C00016 00005	Ray:
C00017 ENDMK
C⊗;
reiter[f82,jmc]		To Reiter re circumscription applied to Nixon paradox

Dear Ray:

	This contains a few changes from version sent on the ARPAnet.

	Here is my treatment of the Nixon paradox.  It uses my new notion
of prioritized circumscription and also the idea of circumscribing a formula
rather than a predicate.  Thus suppose  E{P,x}  is some formula involving
a predicate  P  and a variable  x  with  P  satisfying an axiom  A{P}.
We write

A'{P} ≡ A{P} ∧ ∀P'.A{P'} ∧ (∀x.E{P',x} ⊃ E{P,x}) ⊃ (∀x.E{P,x} ≡ E{P',x})

and call  A'{P}  the circumscription of  E  relative to  A  with  P
as a variable.  This readily generalizes to several variables.  The formula
A'{P}  can be used as the axiom of a further circumscription.
For example, we might want to circumscribe the expression  pacifist x  after
circumscribing  nnly-pacifist  and  nnly-non-pacifist,  thus asserting
that a person is to be considered a pacifist only if there is some reason.

In the Nixon paradox, the axiom  A{nnly-pacifist,nnly-non-pacifist,pacifist} is

(1)	∀x. quaker x ∧ ¬nnly-pacifist x ⊃ pacifist x
	∧ ∀x. republican x ∧ -nnly-non-pacifist x ⊃ ¬pacifist x

	If we make the definition

(2)	A(pp,pnp,p) ≡ (∀x.quaker x ∧ ¬pp x ⊃ p x)
		∧ (∀x.republican x ∧ ¬pnp x ⊃ ¬p x),

then our axiom (1) is  A(nnly-pacifist, nnly-non-pacifist, pacifist).  It
makes the convention that a Quaker is to be considered a pacifist
unless some fact prevents this inference,
and Republican is to be considered a non-pacifist
unless the inference is prevented.  nnly  stands for "not necessarily",
but I hope to find a more perspicuous abbreviation later.

	We circumscribe the expressions  nnly-pacifist x  and
nnly-non-pacifist x  with equal priority using  nnly-pacifist,
nnly-non-pacifist  and  pacifist  as variables of minimization.
The circumscription formula is then

(3)	A(nnly-pacifist,nnly-non-pacifist,pacifist) ∧
	∀pp pnp p.(∀x.quaker x ∧ ¬pp x ⊃ p x)
		∧ (∀x.republican x ∧ ¬pnp x ⊃ ¬p x)
		∧ (∀x.pp x ⊃ nnly-pacifist x) 
		∧ (∀x.pnp x ⊃ nnly-non-pacifist x)
	⊃
		(∀x.nnly-pacifist x ≡ pp x)
		∧ (∀x.nnly-non-pacifist x ≡ pnp x).

	We show that (3) is equivalent to

(4)	A(nnly-pacifist,nnly-non-pacifist,pacifist) ∧
	∧ ∀x.nnly-pacifist x ≡ quaker x ∧ republican x ∧ ¬pacifist x
	∧ ∀x.nnly-non-pacifist x ≡ quaker x ∧ republican x ∧ pacifist x,

which agrees with intuition.

	Going from (3) to (4) requires choosing
the predicates to be subsituted for the variables
pp,  pnp,  and  p.  We make the substitutions

	pp x ≡ quaker x ∧ republican x ∧ ¬pacifist x
	pnp x ≡ quaker x ∧ republican x ∧ pacifist x
	p x ≡ quaker x ∧ ¬republican x
		∨ quaker x ∧ pacifist x
		∨ ¬republican x ∧ pacifist x.

A tedious computation, or the propositional calculus routines of EKL,
show that the left side of (3) is then satisfied, and the right side
then tells us.

(5)	∀x.nnly-pacifist x ≡ quaker x ∧ republican x ∧ ¬pacifist x
	∧ ∀x.nnly-non-pacifist x ≡ quaker x ∧ republican x ∧ pacifist x.

Plugging these into (1) gives

(6)	∀x.quaker x ∧ ¬republican x ⊃ pacifist x
	∧ ∀x.¬quaker x ∧ republican x ⊃ ¬pacifist x,

which is what our intuition tells us should be the result of
taking into account just the facts expressed in (1).  In order
to show that (3) doesn't imply anything about people who are both
Quakers and Republicans, we need to show that (6) implies (3) which
haven't yet got around to doing.

	I'll send you a paper copy of this, because I suppose you
may have difficulty printing the logical symbols, although Bob
Smith, to whom transmit my regards if he's still there, may know
how to print the SAIL character set.
For reference, the special characters are
∀	for all
∃	there exists
∧	and
∨	or
¬	not
{	left curly bracket
}	right curly bracket

	Carolyn and I have proved that when the expression to be
circumscribed has the for  P(x),  your circumscription schema and
mine are equivalent.

Best Regards,
Perhaps we want to say things like

minimize  bird x ∧ ¬can-fly x,

and the minimizations have priorities.

	An extreme view is that we give up axioms altogether.  We have
a language, and we have a partial ordering of interpretations,
and we look for minima in the partial ordering.  To combine this
with another idea, we are really interested in facts about
the partial ordering of interpretations that are independent of
language.  At least we need a way of expressing the partial
ordering that will translate to any interdefinable language.
This is like a change of co-ordinates in geometry.  We would like to
introduce into logic the equivalent of co-ordinate free methods
in geometry.  Perhaps it has already been done.
Some thoughts on circumscription:
 
1. As I remarked in my AAAI talk, but not in the paper, the circumscription
schema for an inductively defined predicate P is provably equivalent to the
axiom of structural induction for P. Let me ellaborate by considering as an
example the sufficient conditions defining an S-expression:
(x)ATOM(x) --> S-EXPR(x)
(xy).S-EXPR(x) & S-EXPR(y) --> S-EXPR(cons(x,y))
 
Circumscribe S-EXPR, replace PHI(x) by S-EXPR(x)&PSI(x), do some simplific-
ation and fidling, and you get
 
[(x).ATOM(x) --> PSI(x)] & [(xy)S-EXPR(x) & PSI(x) & S-EXPR(y) & PSI(y)
--> PSI(cons(x,y))] --> (x).S-EXPR(x) --> PSI(x)
 
This is the usual axiom of structural induction for proving properties of
S-expressions. This is the same construction you used for getting the
induction axiom for the natural numbers in your circumscription paper.
(by the way there is a slight error in your statement of the induction
axiom. What you wrote does not follow logically from your axioms.)
  
Now, what exactly do we mean by an inductive definition? Logicians mean
any set of wffs which are Horn in P. See Barwise's Handbook of Math.
Logic, especially the principle of phi-induction. So my result for theories
Horn in the predicate P says that circumscription is equivalent to the
principle of induction.
 
2. Maybe that's obvious, although it wasn't to me for a long time. But
notice that if T(P) is a theory Horn in P, then
 
T(P & PHI) --> (x).P(x) --> PHI(x)           (1)
 
is equivalent to the axiom of induction for the predicate P. So, let's
generalize the induction axiom to arbitrary theories in P to be exactly
the same formula (1). Maybe logicians have considered this although I
doubt it since they are normally interested in inductively defined sets.
So, my proposal is to define the circumscription schema to be (1) 
rather than your definition.
 
3. Does it work? Well, it does for theories Horn in P as I said earlier.
It also works for the two thorny examples I know about:
 
(a) Circumscribing a disjunction. e.g. your blocks example.
    Take PHI(x) = x=A then x=B as you do in your paper, fiddle a bit, and
    you'll get your formula.
 
(b) Circumscribing an existential. e.g. (Ex)P(x)
    Intuitively, one wants to derive that there is a unique x s.t. P(x)
i.e.
    (Ex)P(x) & [(y)P(y) --> y=x]
    Take PHI(x) = (Ey)P(y) & y=x, fiddle a lot, and you'll get this.
 
What do you think? 
                          Best wishes,
                            Ray
-------

To CLT:
What is your opinion of Reiter's proosal for relating induction schemas
to theories Horn in P and extending it to theories non-Horn in P?

Sorry. there's a bug in example 3(b). Scratch it for now.
-------

Ray:

	Here is Carolyn's proof that your schema implies mine.  We
have yours

(R)	(phi)(T(P&phi) ⊃ (x)(P(x) -→ phi(x))

and we want to prove mine

(J)	(phi)(T(phi) & (x).(phi(x) -→ P(x)) -→ (x)(P(x) -→ phi(x)).

So assume  T(phi) and  (x)(phi(x) -→ P(x)).
The latter formula is equivalent to  (x)(P(x)∧phi(x) iff phi(x)),
from which follows  T(phi) iff T(P&phi).  Hence we can use (R)
to derive the conclusion of (J).

Sorry moving to Rutgers didn't work out, and I hope absence from
Vancouver has made its virtues more apparent.

Regards,

John